/*
 * WinderMatrix.cpp
 *
 * Copyright 2012 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#include "bfr/WinderMatrix.hpp"

#include "bfr/Clause.hpp"
#include "bfr/ClauseSet.hpp"

namespace bfr {

WinderMatrix::WinderMatrix(const ClauseSet *cs, bool create)
    : matrix(0), _size(cs->getMaxLiteralId() + 1) {

    matrix = new size_t*[_size];
    for (size_t i = 0; i < _size; i++) {
        matrix[i] = new size_t[_size + 1];
        for (size_t j = 0; j < _size; j++) {
            matrix[i][j] = 0;
        }
        matrix[i][_size] = i;
    }
    if (create) {
        createEntries(cs);
    }

}

void WinderMatrix::createEntries(const ClauseSet *cs) {
    ClauseSet::const_iterator e = cs->end();
    for (ClauseSet::const_iterator it = cs->begin();
         it != e;
         it++) {
        const Clause *c = *it;
        const size_t cSize = c->size();
        Clause::const_iterator ce = c->end();
        for (Clause::const_iterator cit = c->begin();
             cit != ce;
             cit++) {
            const Literal &l = *cit;
            const size_t lID = l.getId();
            matrix[lID][cSize - 1]++;
        }
    }
}

WinderMatrix::~WinderMatrix() {
    for (size_t i = 0; i < _size; i++) {
        delete[] matrix[i];
    }
    delete[] matrix;
}

void WinderMatrix::swapRows(size_t row1, size_t row2) {
    size_t *buffer = matrix[row1];
    matrix[row1] = matrix[row2];
    matrix[row2] = buffer;
}

}
